es:ES, i:Id, ds:Top, f:k:Knd fp Top, e:E.
((loc(e) = i))  ((e  es-triggers(es;i;ds;f)) ~ ff) 

latex

Definitions	can-apply(f;x), e  X, es-triggers(es;i;ds;conds), Knd, t  T, x. t(x), x:A. B(x), Top, a:A fp B(a), E, loc(e), s = t, , Id, A, P  Q, ES, ff, isl(x), <a, b>, , P  Q, {T}, SQType(T), s ~ t, False, P & Q, b, Type, left + right, True, b, p q, x:AB(x), T, P  Q, x:A  B(x), P  Q, Unit, a = b, kind(e), KindDeq, x  dom(f), p  q
Lemmas	eqtt to assert, assert of band, and functionality wrt iff, eqff to assert, bnot thru band, assert of bor, or functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bor wf, bnot wf, assert wf, band wf, fpf-dom wf, Kind-deq wf, es-kind wf, eq id wf, bool wf, bool sq, not wf, es-loc wf, es-E wf, fpf wf